--------------------------------------------------------------------------------
--
--  Murphi Model of the HyperWall Architecture
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Jason Bau
--  date:         November 2011
--  affiliation:  Stanford University (research assistant)
--
--------------------------------------------------------------------------------
--
--  For now, only modeling the first step of the protocol, which is a request 
--  by a customer to create a VM.
--
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  --first we have the model options.
  CHECKSIGS: true;     --customer checks that signatures are from expected CPU.
  CHECKNONCE: true;    --customer checks that the nonce in the signature is the latest one
  CHECKHS:  false;        --use HS or not in the model.
  CHECKSHADOWVM: false; --should we check the "Shadow VM" invariant?  (Invariant 2)


  NumCustomers:    2;   -- number of Customers
  NumHyperVisors:  1;   -- number of HyperVisors (these are the attackers)
  NumCPUs:         2;   -- number of CPUs
  VMsPerCust:      2;   -- number of VMs each Customer tries to start
  NumVMs:          NumCustomers*VMsPerCust;   -- max number of total VMs
  MaxNonce:        2*NumVMs;  -- max number of nonces
  MaxIMIP:         2*NumVMs;  -- max number of unique (IM,IP) combinations
  NetworkSize:     10;  -- number of requests and responses for VM creation  
  HVMemory:        5;  --number of each signature HV remembers
  HVIP:             0;  --a magic constant (the IMIP for showing Hypervisor Manipulation)
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  CustomerId:    scalarset (NumCustomers);   -- identifiers
  HyperVisorId:  scalarset (NumHyperVisors);
  VMId:          scalarset (NumVMs);
  CPUId:         scalarset (NumCPUs);
  PrincipId:     union {CustomerId, HyperVisorId, CPUId};
  
  CurVM: 1..VMsPerCust;
  Nonce: 1..MaxNonce;
  IMIP:  0..MaxIMIP; -- a serial number for the IM and IP (enumerated together)

  CPUType : enum {
	C_HyperWall,
	C_NoHyperWall
  };

  Known : enum {
    KnownGood,
    KnownBad
  };

  CPU : record
    cType: CPUType
  end;

  VM : record 
    reqBy: PrincipId;            -- who requested me
    cpu: CPUId;                  -- what CPU did this VM start on
    NC: Nonce;                   -- Nonce of last customer request
    IP: IMIP;                    -- Initial protection  
    IM: IMIP;                    -- Initial memory (IP and IM make up SSData)
    PSData: Known;               -- PSData (known good or bad value)
    HSData: Known;               -- HSData (known good or bad value)
  end;

  SS : record                    -- the values preserved by the signed hash.  Attackers can''t write this structure w/o key
    signedBy: PrincipId;         -- what Pricipal signed this
    NC: Nonce;                   -- Nonce of last customer request
    VID: VMId;                   -- which VM Sig refers to
    IP: IMIP;                    -- Initial protection 
    IM: IMIP;                    -- Initial memory 
  end;

  PS : record                    -- the values preserved in the signed hash.  Attackers can''t write this structure w/o key
    signedBy: PrincipId;         -- what prinicpal signed this  
    NC: Nonce;                   -- Nonce of last customer request
    VID: VMId;                   -- which VM Sig refers to
    PSData: Known;               -- PSData (good or bad)
  end;

  HS : record                    -- the values preserved in the signed hash.  Attackers can''t write this structure w/o key
    signedBy: PrincipId;         -- what principal signed this
    NC: Nonce;                   -- Nonce of last customer request
    HSData: Known;               -- HSData (good or bad)
  end;


  MessageType : enum {           -- different types of messages
	M_VMRequest,                 -- request for VM creation
	M_VMResponse                 -- response (ack) for VM creation
  };

  Message : record
    source:   PrincipId;         -- source of message
    dest:     PrincipId;         -- intended destination of message
    mType:    MessageType;       -- type of message
    NC:       Nonce;             -- nonce (NC)
    CPU:      CPUId;             -- which CPU should start the VM (the signature that the customer is expecting).
    IM:       IMIP;              -- IM
    IP:       IMIP;	         -- IP
    SS:       SS;                -- Signature over SSData
    PS:       PS;                -- Signature over PSData
    HS:       HS;                -- Signature over HSData
    HSData:   Known;             -- HSData (either good or bad)
    VID:      VMId;              -- VM Id
  end;


  CustomerStates : enum {
    C_SLEEP,                     -- state after initialization, will request VM creation
    C_WAITFORHV,                 -- customer waiting for VM creation confirmation
    C_COMMIT                     -- customer commits to created VM
  };                             

   
  CustVM : record -- what the customer expects for CPU, IM, IP
    NC: Nonce;	
    CPU: CPUId;
    IM: IMIP;
    IP: IMIP;
    accepted: boolean; --matches expectation?
    VID: VMId;  
  end;

  Customer : record
    state: CustomerStates;
    curVM: CurVM;
    VMs: array[CurVM] of CustVM
  end;                          

  HyperVisorStates : enum {
    H_SLEEP,
    H_DONE
  };

  HyperVisor : record
    state:  HyperVisorStates;
    vms:    array[VMId] of boolean;
    ss: multiset[HVMemory] of SS;
    hs: multiset[HVMemory] of HS;
    ps: multiset[HVMemory] of PS;
    reqs: multiset[HVMemory] of Message; 
  end;

    

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                         -- state variables for
  cust: array[CustomerId] of Customer;      --  Customers
  hype: array[HyperVisorId] of HyperVisor;  --  HyperVisors 
  net:  multiset[NetworkSize] of Message;
  cpu:  array[CPUId] of CPU; 
  vms:  array[VMId] of VM;
  nextNonce:    Nonce;
  nextIMIP:    IMIP;


---functions-------------

-- Generate a fresh nonce

function freshNonce(): Nonce;
var tmp: Nonce;
begin
  if nextNonce = MaxNonce then
     error "Ran out of nonces!"
  end;
  tmp := nextNonce;
  nextNonce := nextNonce + 1;
  return tmp;
end;

-- Generate a next IMIP nonce

function getIMIP(): IMIP;
var tmp: IMIP;
begin
  if nextIMIP = MaxIMIP then
     error "Ran out of IMIPs!"
  end;
  tmp := nextIMIP;
  nextIMIP := nextIMIP + 1;
  return tmp;
end;



--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------
-- behavior of Customers

-- customer i requests VM with HyperVisor j 
ruleset i: CustomerId do
  ruleset j: HyperVisorId do
  ruleset k: CPUId do
    rule 20 "customer requests VM Start"

      cust[i].state = C_SLEEP &
      cust[i].curVM <= VMsPerCust &
      multisetcount (l:net, true) < NetworkSize

    ==>
    
    var
      outM: Message;   -- outgoing message

    begin
      undefine outM;
      outM.source  := i;
      outM.dest    := j;
      outM.mType   := M_VMRequest;
      outM.CPU     := k;
      outM.NC	   := freshNonce();
      outM.IP      := getIMIP();
      outM.IM      := outM.IP;

      multisetadd (outM,net);

      cust[i].VMs[cust[i].curVM].accepted :=false;
      cust[i].VMs[cust[i].curVM].NC       :=outM.NC;
      cust[i].VMs[cust[i].curVM].CPU      :=k;
      cust[i].VMs[cust[i].curVM].IM       := outM.IM;
      cust[i].VMs[cust[i].curVM].IP       := outM.IP;
      cust[i].state                       := C_WAITFORHV;
    end;
  end;
  end;
end;

-- customer i reacts to confirmation received
ruleset i: CustomerId do
  choose j: net do
    rule 20 "customer reacts to confirmation received"

      cust[i].state = C_WAITFORHV &
      net[j].dest = i 
    ==>

    var
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      multisetremove (j,net);

      if inM.mType=M_VMResponse then   -- correct message type
          if ((!CHECKSIGS | inM.SS.signedBy=cust[i].VMs[cust[i].curVM].CPU) & --check signed by right party
			  (!CHECKSIGS | inM.HS.signedBy=cust[i].VMs[cust[i].curVM].CPU) & 
			  (!CHECKSIGS | inM.PS.signedBy=cust[i].VMs[cust[i].curVM].CPU) & 
			  (!CHECKNONCE | inM.SS.NC=cust[i].VMs[cust[i].curVM].NC) &        --check freshness by right nonce
			  (!CHECKNONCE | inM.HS.NC=cust[i].VMs[cust[i].curVM].NC) &  
			  (!CHECKNONCE | inM.PS.NC=cust[i].VMs[cust[i].curVM].NC) & 
			  (inM.SS.VID=inM.PS.VID) &                          --check VIDs for both signatures are same
	                  (inM.SS.IP=cust[i].VMs[cust[i].curVM].IP) &        --checking SS
			  (inM.SS.IM=cust[i].VMs[cust[i].curVM].IM) &
			  (inM.PS.PSData = KnownGood) &                      --checking PS
			  (!CHECKHS | inM.HS.HSData = KnownGood) &             --checking HS
			  (!CHECKHS | inM.HSData = KnownGood)                  --checking HSData
			  )
          then
	    cust[i].VMs[cust[i].curVM].VID := inM.VID;
            cust[i].VMs[cust[i].curVM].accepted := true;            
          else
            --error "initiator received incorrect nonce"
          end;
          if (cust[i].curVM < VMsPerCust) then
            cust[i].state := C_SLEEP;
            cust[i].curVM := cust[i].curVM + 1;
          else
	    cust[i].state := C_COMMIT;
	    --error "did 2"
          end;
       end;
     end;
  end;
end;


--------------------------------------------------------------------------------
-- behavior of HyperVisors
-- appropriate behavior first
-- HyperVisor i reacts to Customer''s request
ruleset i: HyperVisorId do
 ruleset v: VMId do
  choose j: net do
    rule 20 "Hypervisor receives VMStart request, behaves honestly (but records signatures and request)"

      hype[i].state = H_SLEEP &
      net[j].dest = i &
      isundefined(vms[v].reqBy)      --so we don''t overwrite

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
          inM := net[j];
          multisetremove (j,net);


	   --Hypervisor sets data in vm (can manipulate, but doesn''t here)
			vms[v].reqBy:=inM.source;
                        vms[v].cpu:=inM.CPU;
			vms[v].NC:=inM.NC;
			vms[v].IP:=inM.IP;
			vms[v].IM:=inM.IM;
			vms[v].PSData:=KnownGood;
			vms[v].HSData:=KnownGood;
        
          --CPU signs and sends out reply, which the HV does not change
                        undefine outM;
			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;
			outM.VID     := v;

			outM.SS.signedBy:=inM.CPU;
			outM.SS.NC:=inM.NC;
			outM.SS.VID:=v;
			outM.SS.IP:=inM.IP;
			outM.SS.IM:=inM.IM;
			outM.PS.signedBy:=inM.CPU;
                        outM.PS.NC:=inM.NC;
			outM.PS.VID:=v;
			outM.PS.PSData:=KnownGood;
                        outM.HS.signedBy:=inM.CPU;
                        outM.HS.NC:=inM.NC; 
                        outM.HS.HSData:=KnownGood;
	     	        outM.HSData:=KnownGood;

          --Record signatures and request
			multisetadd (outM.PS,hype[i].ps);
			multisetadd (outM.SS,hype[i].ss);
			multisetadd (outM.HS,hype[i].hs);
                        multisetadd (inM,hype[i].reqs);


          --Mark that this VM is controled by this hyperVisor
          hype[i].vms[v]    := true;
          multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
  end; 
 end;
end;


--------------------------------------------------------------------------------
-- behavior of HyperVisors
-- HyperVisor i reacts to Customer''s request
ruleset i: HyperVisorId do
 ruleset v: VMId do
 ruleset c: CPUId do
  choose m: hype[i].reqs do
    rule 20 "Hypervisor starts Shadow VM without any protections, from recorded request"

      hype[i].state = H_SLEEP &
      hype[i].reqs[m].CPU != c &
      isundefined(vms[v].reqBy)      --so we don''t overwrite

    ==>

    var

      inM:  Message;   -- incoming message

    begin
          inM := hype[i].reqs[m];


           --Hypervisor sets data in vm (creating shadow copy)
			vms[v].reqBy:=i;
                        vms[v].cpu:=c;
			vms[v].NC:=inM.NC;
			vms[v].IP:=HVIP;
			vms[v].IM:=inM.IM;
			vms[v].PSData:=KnownGood;
			vms[v].HSData:=KnownGood;
        

                        hype[i].vms[v]    := true;
                        

          --hype[i].state     := H_DONE;
		  
    end;
  end;
 end;
 end;
end;


--------------------------------------------------------------------------------
-- behavior of HyperVisors
-- HyperVisor i reacts to Customer''s request with an attack
ruleset i: HyperVisorId do
 ruleset c: CPUId do
 ruleset v: VMId do
  choose j: net do
    rule 20 "Hypervisor starts bad VM then signs with its own signature in ack"

      hype[i].state = H_SLEEP &
      net[j].dest = i &
      isundefined(vms[v].reqBy)      --so we don''t overwrite

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
          inM := net[j];
          multisetremove (j,net);


		  --Hypervisor sets data in vm (with manipulated value)
			vms[v].reqBy:=i;
                        vms[v].cpu:=c;
			vms[v].NC:=inM.NC;
                        vms[v].IP:=HVIP;
			vms[v].IM:=vms[v].IP;
			vms[v].PSData:=KnownBad;
			vms[v].HSData:=KnownBad;
        
          --Hypervisor sends message pretending started VM is OK, but HV has to sign instead of the CPU
                        undefine outM;
			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;
			outM.VID     := v;

			outM.SS.signedBy:=i; --Hypervisor signs, not CPU
			outM.SS.NC:=inM.NC;
			outM.SS.VID:=v;
			outM.SS.IP:=inM.IM;
			outM.SS.IM:=inM.IP;
			outM.PS.signedBy:=i; --Hypervisor signs, not CPU
                        outM.PS.NC:=inM.NC;
			outM.PS.VID:=v;
			outM.PS.PSData:=KnownGood;
                        outM.HS.signedBy:=i; --Hypervisor signs, not CPU
                        outM.HS.NC:=inM.NC; 
                        outM.HS.HSData:=KnownGood;
		        outM.HSData:=KnownGood;


          --Mark that this VM is controled by this hyperVisor
          hype[i].vms[v]    := true;

          multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
  end; 
 end;
 end;
end;


--------------------------------------------------------------------------------
-- behavior of HyperVisors
-- HyperVisor i reacts to Customer''s request with an attack
ruleset i: HyperVisorId do
 ruleset c: CPUId do
 ruleset v: VMId do
   choose s: hype[i].ss do
   choose h: hype[i].hs do
   choose p: hype[i].ps do
   choose j: net do
    rule 20 "Hypervisor starts bad VM then uses recorded signature in ack"

      hype[i].state = H_SLEEP &
      net[j].dest = i &
      isundefined(vms[v].reqBy)      --so we don''t overwrite

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message
    begin
          inM := net[j];
          multisetremove (j,net);


          --Hypervisor sets data in vm (changes to bad values)
			vms[v].reqBy:=i;
                        vms[v].cpu:=c;
			vms[v].NC:=inM.NC;
                        vms[v].IP:=HVIP;
			vms[v].IM:=vms[v].IP;
			vms[v].PSData:=KnownBad;
			vms[v].HSData:=KnownBad;
        
          --User recorded Signatures to try to fool customer
                        undefine outM;
			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;
			outM.VID     := v;
	   	        outM.HS      := hype[i].hs[h];
                        outM.PS      := hype[i].ps[p];
                        outM.SS      := hype[i].ss[s];
		        outM.HSData  := KnownGood;


          --Mark that this VM is controled by this hyperVisor
          hype[i].vms[v]    := true;

          multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
    end;
    end;
    end;
  end; 
 end;
 end;
end;



--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  nextNonce := 1;
  nextIMIP := 1;
  -- initialize initiators
  undefine cust;
  for i: CustomerId do
    cust[i].state     := C_SLEEP;
    for j: CurVM do
      cust[i].VMs[j].accepted:=false;
      cust[i].curVM := 1;
    end;
  end;

  -- initialize HyperVisors
  undefine hype;
  for i: HyperVisorId do
    hype[i].state     := H_SLEEP;
      for j:VMId do
        hype[i].vms[j] := false;
      end;
  end;

  -- initialze CPUs
  undefine cpu; 
  for i: CPUId do 
    cpu[i].cType  := C_HyperWall;
  end;
 
  -- initialize everything else
  undefine net;
  undefine vms;

end;



--------------------------------------------------------------------------------
-- invariants
--------------------------------------------------------------------------------

-- invariant 1a) "Started VM is identified by VID" is always satisfied (it just instantiates an identifier)
invariant "vms start with customer expectation"
forall i: CustomerId do
   forall j: CurVM do
      cust[i].state = C_COMMIT &
      cust[i].VMs[j].accepted
	   ->
	  vms[cust[i].VMs[j].VID].cpu = cust[i].VMs[j].CPU & --invariant 1b) VM started on a CPU that the customer expects
	  vms[cust[i].VMs[j].VID].IP = cust[i].VMs[j].IP &   --invariant 1c) IP as set by customer
          vms[cust[i].VMs[j].VID].IM = cust[i].VMs[j].IM &   --invariant 1c) IM as set by customer
	  vms[cust[i].VMs[j].VID].PSData = KnownGood &       --invariant 1d) Good PSData
	  (!CHECKHS | vms[cust[i].VMs[j].VID].HSData = KnownGood) --invariant 1e) Good HSData
   end
end;


--invariant "no shadow copy vms"  --Invariant 2
ruleset i: VMId do               
 ruleset j: VMId do
  rule 20 "no shadow copy vms" 
    CHECKSHADOWVM & --check this invariant?
    (i != j) &                                      -- for any 2 different VMs, i and j
    !isundefined(vms[i].IP) & vms[i].IP  != HVIP &  -- if i has been started with original IP and IM, not manipulated by HV  
    !isundefined(vms[i].IM) & vms[i].IM  != HVIP &  -- and
    !isundefined(vms[j].IP) & vms[j].IP  = HVIP &   -- if j has been started with IP manipulated by HV
    !isundefined(vms[j].IM) & vms[j].IM = vms[i].IM -- and with IM identical to that for i 
    ==> 
    error "shadow copy found!"                      -- this is a dirty trick shadow copy
    end;
  end;
end;
